$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$). retraction($T$;$f$) $\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($x$ = $y$)) $\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($x$ is $f$$\ast$($y$)))